Coq (proof assistant system)
Public.icon
Coq is a proof assistant system. The core of Coq uses the programming language Gallina. It is being developed by the PI.R2 team of the French National Institute for Computer Science and Control (located within the PPS research institute), in collaboration with École Polytechnique, the National School of Arts and Crafts, Paris Diderot University, Paris-Sud University (formerly also with the École Normale Supérieure de Lyon). Hugo Herbelin is the de facto development leader. https://gyazo.com/ba3b9998bf258aa44a727ab3ff480349